/* Copyright(C) 2000, Swedish Institute of Computer Science */

/*! \todo Drop the restriction on bounded domains with respect to side
          constraints. 
*/

/*! \todo What is a good max size for the trail? */

/*
   The linear inequalities in this constraint are propagated using
   techniques described in the paper "Bounds Consistenc Techniques for
   Long Linear Constraints" by Warwick Harvey and Joachim Schimpf.

   CASE_STAR enables case extended with linear arithmetic.

   CASE_INCF is an optimization to maintain false nodes on O(1) time.

   CASE_INC  is an optimization to maintain a small set of true nodes,
   but it is BROKEN.  Witness:

   | ?- domain([X,Y,Z],0,1), table([[1,0,Z],[Z,0,X],[Z,Y,X]],[[1,0,0],[0,1,0],[0,0,1]]).
   X = 1,
   Z = 0,
   Y in 0..1 ? 

 */

#include "fd.h"
#include "dvars.h"

#define CASE_INC  0
#define CASE_INCF 1
#define CASE_STAR 1

#if MULTI_SP_AWARE
#define eval_dag(A1,A2,A3) eval_dag(HIDDEN_ARG, A1,A2,A3)
#if CASE_STAR
#define eval_dag_star(A1,A2,A3) eval_dag_star(HIDDEN_ARG, A1,A2,A3)
#endif /* CASE_STAR */
#define compute_prune_sets(A,B,C) compute_prune_sets(HIDDEN_ARG,A,B,C)
#define queue_push(A1, A2) queue_push(HIDDEN_ARG, A1, A2)
#define queue_pop(A) queue_pop(HIDDEN_ARG, A)
#define trail(A1,A2,A3,A4,A5,A6) trail(HIDDEN_ARG,A1,A2,A3,A4,A5,A6)
#define untrail(A1) untrail(HIDDEN_ARG, A1)
#define update_and_enqueue(A1,A2,A3,A4,A5,A6,A7) update_and_enqueue(HIDDEN_ARG,A1,A2,A3,A4,A5,A6,A7)
#define propagate(A1,A2) propagate(HIDDEN_ARG, A1, A2)
#define initialize_and_enqueue(A1,A2) initialize_and_enqueue(HIDDEN_ARG,A1,A2)
#define prune_store_prune_sets(A1,A2,A3) prune_store_prune_sets(HIDDEN_ARG,A1,A2,A3)
#endif /* MULTI_SP_AWARE */

#define CASE_DOM 0
#define CASE_MINMAX 1
#define CASE_MIN 2
#define CASE_MAX 3
#define CASE_VAL 4
#define CASE_NONE 5

#if CASE_STAR
#define DEBUG_HEAP 0

#define B1 0x1
#define B2 0x2
#define B3 0x4
#define B4 0x8
#define B5 0x10
#define B6 0x20

typedef enum {
  T_LOWER  = B1,       /* 00000001 */
  T_I      = B2|B1,    /* 00000011 */
  T_UPPER  = B3|B1,    /* 00000101 */
  T_E      = B4|B1,    /* 00001001 */
  T_F      = B5|B1,    /* 00010001 */
  T_ACTIVE = B6|B1     /* 00100001 */
} trailed;

#define NTRAILED 6

typedef enum {ACTIVE=B1, QUEUED=B2} linear_status;

#endif /* CASE_STAR */

struct case_data {
  void (SPCDECL *destructor)(void*);
  void (SPCDECL *daemon)(HIDDEN_PROTO
			 Argtype,void *,SP_globref,TAGGED); /* (w,handle,attr_ref,global) */
#if MULTI_SP_AWARE
  SPEnv *spenv;
#endif /* MULTI_SP_AWARE */

  SP_globref refbase;
  long stamp;			/* increases up to backtracking */
  long first;			/* head of (-1)-terminated list of queued rows */
  long *next;			/* next[i]==(-2) iff not in the queue */
  int nrefs;
  int nrows;
  int nvars;
  int nnodes;
#if CASE_STAR
  unsigned int nlinears;        /* total number of linears */
#endif /* CASE_STAR */
  int prune_set_end;
  SP_BOOL entailed;		/* entailment flag for current row */
  unsigned long false_date;	/* even */
  unsigned long true_date;	/* off */
  Dvar dvar;
  TAGGED *prune_set;
  TAGGED *cache_set;
  unsigned long *control;
  unsigned long *on;
  unsigned long *latest_date;
  unsigned long *latest_daterow;
  long *latest_size;
  struct {
    unsigned long *date;	/* TRUE(FALSE) if = true_date(false_date), undefined otherwise */
    unsigned long *daterow;
    long *id;			/* unique by definition */
    long *var_index;
    long *child_index;
    long *child_end;            
#if CASE_STAR
    SP_BOOL *safe;              /* true iff this node can be flagged true/false 
                                   when visited, this depends on the side 
				   constraints */
#endif /* CASE_STAR */
  } dag_node;
  struct {
    TAGGED *min, *max;
#if CASE_STAR
    unsigned long *linear_index; /* start index of linears for the child */
    unsigned long *linear_end;   /* end index of linears for the child */
#endif /* CASE_STAR */
    long *node_index;
  } child;
#if CASE_STAR
  struct {
    long *a;                    /* coefficients */
    long *x;                    /* variable indices (wrt case) */
    long *b;                    /* bound */
    unsigned long *length;
    linear_status *status;
    long *E;                    /* see the paper above, maintain */
    long *F;                    /* see the paper above, maintain */
    long *I;                    /* see the paper above, maintain */
    unsigned long *heap;        /* max heap of Is for 0<=i<length, maintain */
    unsigned long *heapx;       /* indices for constant heap access, maintain */
  } linear;
  struct {
    long *min, *max;            /* current min and max according to dag traversal
                                   for variables in store */
    unsigned long *queue;       /* queue of linears to propagate */
    unsigned long nqueue;       
    unsigned long nactive;      /* number of active linears */
    unsigned long *vars;        /* store variables' indices */
    unsigned long nvars;        /* number of store variables */
  } store;
  struct {
    trailed *type;
    unsigned long *date;
    unsigned long *i;
    unsigned long *j;
    long *value;
    long size;
    long max_size;
  } trail;
  unsigned long *degree;  /* number of attached constraints for each variable */
  unsigned long *linears; /* list of linears for each variable */
  unsigned long *indices; /* list of indices in linears for each variable */
#endif /* CASE_STAR */
#if CASE_INCF
  struct {
    unsigned long *dense;
    unsigned long *denserow;
    unsigned long *sparse;
    unsigned long *sparserow;
    unsigned long cardinality;
  } false_nodes;
#endif /* CASE_INCF */
};

#define DVAR(N) (pdata->dvar+(N))
#define DATE(R,N) (pdata->dag_node.date[nnodes*(R)+(N)])
#define DATErow(N) (pdata->dag_node.daterow[N])
#define ID(N) (pdata->dag_node.id[N])
#define VAR(N) (pdata->dag_node.var_index[N])
#define CHILD(N) (pdata->dag_node.child_index[N])
#define CHILD_END(N) (pdata->dag_node.child_end[N])
#define ATTRIBUTE_LOC(R,C) (pdata->refbase+((nvars*(R)+(C))<<1))
#define ENT_FLAG(R) RefGlob(pdata->refbase+2*nrows*nvars+(R))
#define CMIN(Ch) (pdata->child.min[Ch])
#define CMAX(Ch) (pdata->child.max[Ch])
#define NODE(Ch) (pdata->child.node_index[Ch])
#define LATEST_DATE(R,C) (pdata->latest_date[nvars*(R)+(C)])
#define LATEST_DATErow(C) (pdata->latest_daterow[C])
#define LATEST_SIZE(R,C) (pdata->latest_size[nvars*(R)+(C)])

#if CASE_STAR
#define SAFE(N) (pdata->dag_node.safe[N])
#define LINEAR(C) (pdata->child.linear_index[C])
#define LINEAR_END(C) (pdata->child.linear_end[C])
#define LINEAR_A(L) (pdata->linear.a+((L)*pdata->nvars))
#define LINEAR_X(L) (pdata->linear.x+((L)*pdata->nvars))
#define LINEAR_B(L) (pdata->linear.b[L])
#define LINEAR_F(L) (pdata->linear.F[L])
#define LINEAR_E(L) (pdata->linear.E[L])
#define LINEAR_I(L) (pdata->linear.I+((L)*pdata->nvars))
#define LINEAR_LENGTH(L) (pdata->linear.length[L])
#define LINEAR_STATUS(L) (pdata->linear.status[L])
#define LINEAR_HEAP(L) (pdata->linear.heap+((L)*pdata->nvars))
#define LINEAR_HEAPX(L) (pdata->linear.heapx+((L)*pdata->nvars))
#define SMIN(I) (pdata->store.min[(I)])
#define SMAX(I) (pdata->store.max[(I)])
#define DEGREE(X) (pdata->degree[X])
#define VAR_LINEAR(X,I) (pdata->linears[pdata->nlinears*(X)+I])
#define VAR_LINEAR_INDEX(X,I) (pdata->indices[pdata->nlinears*(X)+I])
#define LATEST_TRAIL_DATE() (pdata->trail.date[pdata->trail.size-1])

#define ACTIVATE(L)					\
{							\
  SP_ASSERT(!LINEAR_STATUS(L));				\
  LINEAR_STATUS(L) = ACTIVE;				\
  pdata->store.nactive++;				\
}							\

/* [MA] Deactivate linears as early as possible! */
#define DEACTIVATE(L)					\
{							\
  pdata->store.nactive--;				\
  LINEAR_STATUS(L) ^= ACTIVE;				\
}							\

static INLINE long floor_div(long dividend, long divisor) {
  long q = dividend / divisor;
  return q >= 0 ? q : q - (dividend / divisor != 0);
}

static INLINE long ceil_div(long dividend, long divisor) {
  long q = dividend / divisor;

  return q >= 0 ? q + (dividend / divisor != 0) : q;
}

SP_BOOL verify_heap(unsigned long *heap, long *key, unsigned long size);

SP_BOOL verify_heap(unsigned long *heap, long *key, unsigned long size) {
  unsigned long i;

  for (i=0; i<size; i++) {
    unsigned long l = (i<<1)+1;
    unsigned long r = l+1;

    if ((l < size && key[heap[i]] < key[heap[l]])
	|| (r < size && key[heap[i]] < key[heap[r]]))
      return FALSE;
  }

  return TRUE;
}

#define HEAP_SWAP(I,J)				\
{						\
  unsigned long xi = heap[I];			\
  unsigned long xj = heap[J];			\
  heap[I] = xj;					\
  heap[J] = xi;					\
  heapx[xi] = (J);				\
  heapx[xj] = (I);				\
}

static INLINE void sift_down(struct case_data *pdata,
			     unsigned long linear,
			     unsigned long i) {
  unsigned long *heap = LINEAR_HEAP(linear);
  unsigned long *heapx = LINEAR_HEAPX(linear);
  long *I = LINEAR_I(linear);
  unsigned long size = LINEAR_LENGTH(linear);
  
  while (TRUE) {
    unsigned long l = (i<<1)+1;
    unsigned long r = l+1;
    unsigned long topmost = i;
    if (l<size && I[heap[l]] > I[heap[topmost]])
      topmost = l;
    if (r<size && I[heap[r]] > I[heap[topmost]])
      topmost = r;
    if (topmost==i)
      break;
    HEAP_SWAP(i,topmost);
    i = topmost;
  }
}

static INLINE void sift_up(struct case_data *pdata,
			   unsigned long linear,
			   unsigned long i) {
  unsigned long *heap = LINEAR_HEAP(linear);
  unsigned long *heapx = LINEAR_HEAPX(linear);
  long *I = LINEAR_I(linear);
  
  while (i>0) {
    unsigned long p = (i-1)>>1;
    unsigned long lowest = i;
    if (i>0 && I[heap[p]] < I[heap[lowest]])
      lowest = p;
    if (lowest==i)
      break;
    HEAP_SWAP(i,lowest);
    i = lowest;
  }
}

static INLINE void queue_push MAGIC (HIDDEN_PROTO
				     struct case_data *pdata, 
				     unsigned long linear) {
  HIDDEN_ARG_USE;
  SP_ASSERT(LINEAR_STATUS(linear) & ACTIVE 
	    && !(LINEAR_STATUS(linear) & QUEUED)
	    && pdata->store.nqueue < pdata->nlinears);
  pdata->store.queue[pdata->store.nqueue++] = linear;
  LINEAR_STATUS(linear) |= QUEUED;					
}									
    
static INLINE unsigned long queue_pop MAGIC (HIDDEN_PROTO 
					     struct case_data *pdata) 
{
  unsigned long linear;
  HIDDEN_ARG_USE;
  SP_ASSERT(pdata->store.nqueue > 0);
  linear = pdata->store.queue[--pdata->store.nqueue];
  SP_ASSERT(LINEAR_STATUS(linear) & QUEUED);
  LINEAR_STATUS(linear) ^= QUEUED;
  return linear;
}					

static INLINE void trail MAGIC (HIDDEN_PROTO
				struct case_data *pdata,
				trailed type,
				unsigned long date,
				unsigned long i,
				unsigned long j,
				long value) {
  unsigned long index = pdata->trail.size;

  if (index == pdata->trail.max_size) {
    long max_size = pdata->trail.max_size * 2;
    pdata->trail.type = 
      Realloc(pdata->trail.type, max_size, trailed);
    pdata->trail.date = 
      Realloc(pdata->trail.date, max_size, unsigned long);
    pdata->trail.i = 
      Realloc(pdata->trail.i, max_size, unsigned long);
    pdata->trail.j = 
      Realloc(pdata->trail.j, max_size, unsigned long);
    pdata->trail.value = 
      Realloc(pdata->trail.value, max_size, long);
    pdata->trail.max_size = max_size;
  }

  pdata->trail.type[index] = type;
  pdata->trail.date[index] = date;

  if (type & 0x1)
    pdata->trail.i[index] = i;

  if (type & 0x2)
    pdata->trail.j[index] = j;

  pdata->trail.value[index] = value;

  pdata->trail.size = index + 1;
}


static INLINE void untrail MAGIC (HIDDEN_PROTO
				  struct case_data *pdata) {
  unsigned long index, i, j;
  long value, tmp;

  HIDDEN_ARG_USE;
  SP_ASSERT(pdata->trail.size > 0);  

  index = pdata->trail.size - 1;
  i = pdata->trail.i[index];
  j = pdata->trail.j[index];
  value = pdata->trail.value[index];

  switch (pdata->trail.type[index]) {
  case T_LOWER: /* i=x */
    SP_ASSERT(DEGREE(i));
    SMIN(i) = value;
    break;
  case T_UPPER: /* i=x */
    SP_ASSERT(DEGREE(i));
    SMAX(i) = value;
    break;
  case T_E: /* i=linear */
    LINEAR_E(i) = value;
    break;
  case T_F: /* i=linear */
    LINEAR_F(i) = value;
    break;
  case T_I: /* i=linear, j=x_i */ 
    tmp = LINEAR_I(i)[j];
    LINEAR_I(i)[j] = value;
    if (tmp > LINEAR_I(i)[j]) 
      sift_down(pdata, i, LINEAR_HEAPX(i)[j]);
    else
      sift_up(pdata, i, LINEAR_HEAPX(i)[j]);
#if DEBUG_HEAP
    SP_ASSERT(verify_heap(LINEAR_HEAP(i), LINEAR_I(i), LINEAR_LENGTH(i)));
#endif /* DEBUG_HEAP */
    break;
  case T_ACTIVE: /* i=linear */
    ACTIVATE(i);
    break;
  }

  pdata->trail.size = index;
}

/* 
   Updates the bound of x and the data structures of any linear
   inequality of x. Possible schedules the linear inequalities of x
   for propagation, or fails or entails them.
 */
static INLINE SP_BOOL update_and_enqueue MAGIC (HIDDEN_PROTO
						struct case_data *pdata,
						int x,
						trailed which_bound,
						long old_bound,
						long new_bound,
						unsigned long date,
						unsigned long trigger)
{
  unsigned long i;
  long temp_min, temp_max;
  TAGGED set;

#if DBG
  long smin0 = SMIN(x);
  long smax0 = SMAX(x);
#endif /* DBG */

  SP_ASSERT(DEGREE(x));

  SP_ASSERT(old_bound != new_bound);

  set = pdata->cache_set[x];

  trail(pdata, which_bound, date, x, 0 /* dummy */, old_bound);
  if (which_bound == T_LOWER) {
    fd_intersection_interval_min_max_l(set, MakeSmall(new_bound), 
				       MakeSmall(CLPFD_MAXINT4), 
				       &temp_min, &temp_max);
    new_bound = temp_min;
    SMIN(x) = new_bound;
  }
  else { /* which_bound == T_UPPER */
    fd_intersection_interval_min_max_l(set, MakeSmall(-CLPFD_MAXINT4), 
				       MakeSmall(new_bound), &temp_min, &temp_max);
    new_bound = temp_max;
    SMAX(x) = new_bound;
  }

  SP_ASSERT(fd_member(MakeSmall(new_bound), set));

  if (SMIN(x) > SMAX(x))  /* domain wipe-out */
    return FALSE;

  for (i=0; i<DEGREE(x); i++) {
    unsigned long linear = VAR_LINEAR(x, i);
    linear_status status = LINEAR_STATUS(linear);

    if (status&ACTIVE) {
      long x_i = VAR_LINEAR_INDEX(x, i);
      long a_x = LINEAR_A(linear)[x_i];
      long I_x = LINEAR_I(linear)[x_i];

      SP_ASSERT(LINEAR_X(linear)[x_i] == x);
#if DBG
      SP_ASSERT(I_x == ABS(a_x) * (smax0 - smin0));
#endif /* DBG */

      trail(pdata, T_I, date, linear, x_i, I_x);
      LINEAR_I(linear)[x_i] = ABS(a_x) * (SMAX(x) - SMIN(x));

      if (I_x > LINEAR_I(linear)[x_i])
	sift_down(pdata, linear, LINEAR_HEAPX(linear)[x_i]);
      else
	sift_up(pdata, linear, LINEAR_HEAPX(linear)[x_i]);
      
#if DEBUG_HEAP
      SP_ASSERT(verify_heap(LINEAR_HEAP(linear), 
			    LINEAR_I(linear), 
			    LINEAR_LENGTH(linear)));
#endif /* DEBUG_HEAP */

      if ((a_x > 0 && which_bound == T_UPPER)
	  || (a_x < 0 && which_bound == T_LOWER)) {
	trail(pdata, T_E, date, linear, 0 /* dummy */, LINEAR_E(linear));
	LINEAR_E(linear) += a_x * (new_bound - old_bound);
 	if (LINEAR_E(linear) <= 0) { /* entailed */
 	  trail(pdata, T_ACTIVE, date, linear, 0 /* dummy */, status);
 	  DEACTIVATE(linear);
	}
      }
      else if ((a_x > 0 && which_bound == T_LOWER)
	       || (a_x < 0 && which_bound == T_UPPER)) {
	trail(pdata, T_F, date, linear, 0 /* dummy */, LINEAR_F(linear));
	LINEAR_F(linear) += a_x * (old_bound - new_bound);
	if (LINEAR_F(linear) < 0) /* failed */
	  return FALSE;
	
	if (!(status&QUEUED) && linear != trigger) 
	  queue_push(pdata, linear);
      }
    }
  }

  return TRUE;
}

/* 
   Propagates each constraint in the store (until failure). 
 */
static INLINE SP_BOOL propagate MAGIC (HIDDEN_PROTO 
				       struct case_data *pdata, 
				       unsigned long col) {
  SP_BOOL state = TRUE;

  SP_ASSERT(col < pdata->nvars);

  while (state && pdata->store.nqueue) {
    unsigned long linear = queue_pop(pdata);
    linear_status status = LINEAR_STATUS(linear);
    long *a = LINEAR_A(linear);
    long *x = LINEAR_X(linear);
    long F = LINEAR_F(linear);
    long *I = LINEAR_I(linear);
    unsigned long *heap = LINEAR_HEAP(linear);

    if (!(status&ACTIVE))
      continue;

    while(state && I[heap[0]] > F) {
      unsigned long xi = heap[0];
      long oldmin = SMIN(x[xi]);
      long oldmax = SMAX(x[xi]);

      SP_ASSERT(DEGREE(x[xi]));

      if (a[xi] > 0) {
	long newmax = floor_div(F, a[xi]) + oldmin;
	/* [MA] 20101119: if newmax \notin domain x[xi] we can set it
	   to the next lower value, right? */
	if (newmax < oldmax) {
	  state &= (newmax >= oldmin && 
		    update_and_enqueue(pdata, x[xi], T_UPPER, oldmax, newmax,
				       col, linear));
	}
      }
      else { /* a[xi] < 0 */
	long newmin = ceil_div(F, a[xi]) + oldmax;
	/* [MA] 20101119: if newmin \notin domain x[xi] we can set it
	   to the next higher value, right? */
	if (newmin > oldmin) {
	  state &= (newmin <= oldmax &&
		    update_and_enqueue(pdata, x[xi], T_LOWER, oldmin, 
				       newmin, col, linear));
	}
      }
    }
  }

  return state;
}

/* 
   Initializes the data structures of the linear, possibly schedules
   it for propagation, or fails or entails it.
*/
static INLINE SP_BOOL initialize_and_enqueue MAGIC (HIDDEN_PROTO
						    struct case_data *pdata,
						    unsigned long linear) {
  unsigned long i;
  long *a = LINEAR_A(linear);
  long *x = LINEAR_X(linear);
  long F = LINEAR_B(linear);
  long E = -F;
  long *I = LINEAR_I(linear);
  unsigned long length = LINEAR_LENGTH(linear);

  SP_ASSERT(!LINEAR_STATUS(linear));

  ACTIVATE(linear);

  for (i=0; i<length; i++) {
    long smin = SMIN(x[i]);
    long smax = SMAX(x[i]);

    SP_ASSERT(DEGREE(x[i]));

    if (a[i] > 0) {
      E += a[i]*smax;
      F -= a[i]*smin;
    }
    else { /* a[i] < 0 */
      SP_ASSERT(a[i] < 0);
      E += a[i]*smin;
      F -= a[i]*smax;
    }

    I[i] = ABS(a[i]) * (smax - smin);
  }

  LINEAR_E(linear) = E;
  LINEAR_F(linear) = F;

  if (F < 0) /* failed */ {
    return FALSE;
  }
  else if (E <= 0) { /* entailed */ 
    DEACTIVATE(linear);
  }
  else {
    for (i=length-1; i--; ) sift_down(pdata, linear, i);
#if DEBUG_HEAP
    SP_ASSERT(verify_heap(LINEAR_HEAP(linear), I, length));
#endif /* DEBUG_HEAP */
    queue_push(pdata, linear);
  }

  return TRUE;
}									

/* 
   Prunes the prune sets of each variable in the store until col. Note
   that the prune set of a store variable may be pruned several times
   at a given node, since the linear inequalities may affect the store
   bounds for those variables in different ways along different paths.
 */
static INLINE void prune_store_prune_sets MAGIC (HIDDEN_PROTO Argdecl,
					   struct case_data *pdata,
					   unsigned long col) {
  unsigned long x;

  /*
    [MA] Optimize so that only relevant variables are pruned! This can
    be done by keeping a stack of the currently touched store
    variables in place of the store.vars array, and pushing/popping
    variables when these go in/out of scope.
   */

  for (x=0; x<pdata->store.nvars && pdata->store.vars[x] < col; x++) {
    unsigned long x_i = pdata->store.vars[x];
    TAGGED smin = MakeSmall(SMIN(x_i));
    TAGGED smax = MakeSmall(SMAX(x_i));

    SP_ASSERT(DEGREE(x_i));

    /* [MA] Do something when the prune set is empty? */
    pdata->prune_set[x_i] = 
      fd_subtract_interval(w, pdata->prune_set[x_i], smin, smax);
  }
}


#endif /* CASE_STAR */

#if CASE_INCF
#define FALSE_DENSE(R,N) (pdata->false_nodes.dense[nnodes*(R)+(N)])
#define FALSE_DENSErow(N) (pdata->false_nodes.denserow[N])
#define FALSE_SPARSE(R,N) (pdata->false_nodes.sparse[nnodes*(R)+(N)])
#define FALSE_SPARSErow(N) (pdata->false_nodes.sparserow[N])
#define FALSE_CARD_MUT(R) RefGlob(pdata->refbase+2*nrows*nvars+nrows+(R))

static void false_add(struct case_data *pdata,int node)
{
  unsigned long n = pdata->false_nodes.cardinality;
  
  FALSE_SPARSErow(node) = n;
  FALSE_DENSErow(n) = node;
  pdata->false_nodes.cardinality = n+1;
}
#endif /* CASE_INCF */

static void SPCDECL case_destructor(void *pdata_v)
{
  struct case_data *pdata = (struct case_data *)pdata_v;
  FD_SETUP_SPENV(pdata->spenv);

  SP_free_globrefs(pdata->refbase,pdata->nrefs);
  SP_free(pdata);
}

static int 
compute_prune_sets MAGIC(HIDDEN_PROTO
			 struct case_data *pdata,
			 Argdecl,
			 int row)
{
  int nvars = pdata->nvars;
  int nnonground = 0;
  unsigned int i;
  
  for (i=0; i < nvars; i++) {
    SP_globref ref = ATTRIBUTE_LOC(row,i);
    Dvar dv = DVAR(i);
    
    dvar_init(dv, ref, ref+1);
    pdata->cache_set[i] = pdata->prune_set[i] = dvar_set(dv,w);
    nnonground += !dvar_is_integer(dv);
  }
  pdata->prune_set_end = nvars;
  return nnonground;
}

static void SPCDECL 
case_daemon MAGIC (HIDDEN_PROTO
		   Argdecl,
		   void *vdata,
		   SP_globref attr_ref,
		   TAGGED global)
{
  struct case_data *pdata = (struct case_data *)vdata;
  int nrows = pdata->nrows;
  int nvars = pdata->nvars;
  TAGGED t, tstate;
  int ar, row, col, state_stamp;
  long f, n;
  Dvar dv;

  row =  (attr_ref - pdata->refbase)/(pdata->nvars<<1);
  col = ((attr_ref - pdata->refbase)%(pdata->nvars<<1))>>1;
  t = ENT_FLAG(row);
  DerefSwitch(t,goto cont;);
  return;
 cont:
  w->numstack_end = NULL;
  dv = DVAR(col);
  dvar_init(dv, attr_ref, attr_ref+1);
  tstate = RefMutable(CTagToArg(global,1));
  ar = Arity(TagToHeadfunctor(tstate));
  state_stamp = GetSmall(CTagToArg(tstate,ar));
  if (pdata->stamp!=state_stamp) { /* non-incremental */
    for (f = pdata->first; f != -1; f = n) {
      n = pdata->next[f];
      pdata->next[f] = -2;
    }
    pdata->first = -1;
    pdata->stamp = state_stamp;
    pdata->false_date += 2;
    pdata->true_date += 2;
  } else if (LATEST_DATE(row,col)==pdata->true_date &&
	     LATEST_SIZE(row,col)==dvar_value_count(dv)) {
    return;			/* self-invocation */
  }
#if CASE_INC
 {
   int i;
   for (i=col; i>=0; i--) {
     if (LATEST_DATE(row,i) == -1U)
       break;
     LATEST_DATE(row,i) = -1U;
   }
 }
#endif /* CASE_INC */
  if (pdata->first == -1) {
    int q;
    (void)fd_daemon_copy_state(w,&global);
    pdata->stamp++;
    switch (pdata->on[col]) {
    case CASE_MIN:
    case CASE_MAX:
    case CASE_MINMAX:
      q = 0x5;
      break;
    case CASE_VAL:
      q = 0x3;
      break;
    case CASE_DOM:
    default:
      q = 0x7;
    }
    fd_enqueue_global(w, global, q);
  }
  if (pdata->next[row] == -2) {
    pdata->next[row] = pdata->first;
    pdata->first = row;
  }
}


static int eval_dag MAGIC (HIDDEN_PROTO Argdecl,
			   int node,
			   struct case_data *pdata)
{
  unsigned long date = DATErow(node);
  int col = VAR(node);
  int state = FALSE;

  SP_ASSERT(0 <= node && node < pdata->nnodes);

    if (date & 0x1) {		/* TRUE or unknown */
      if (date == pdata->true_date) {
	return TRUE;
      }
#if CASE_INC
      if (col>=pdata->prune_set_end && date >= LATEST_DATErow(col)) {
	DATErow(node) = pdata->true_date;
	return TRUE;
      }
#endif /* CASE_INC */
    } else {			/* FALSE or unknown */
      if (date == pdata->false_date)
	return FALSE;
#if CASE_INCF
      {
	unsigned long fsp = FALSE_SPARSErow(node);
  
	if (fsp < pdata->false_nodes.cardinality && FALSE_DENSErow(fsp)==node) {
	  DATErow(node) = pdata->false_date;
	  return FALSE;
	}
      }
#endif /* CASE_INCF */
    }
  {
    Dvar dv = DVAR(col);
    int child = CHILD(node);
    int child_end = CHILD_END(node);
    TAGGED set = pdata->cache_set[col];
    TAGGED min = dvar_min_t(dv);
    TAGGED max = dvar_max_t(dv);

    if (min!=CMIN(child)) {
      /* dichotomic search for first child */
      int sup = child_end;
      while (child<sup) {
	int mid = (child+sup)>>1;
	if (FDgt(min,CMAX(mid)))
	  child = mid+1;
	else
	  sup = mid;
      }
    }
    
    /* scan the compatible children */
    while (child < child_end &&
	   FDle(CMIN(child),max) &&
	   (!state || col+1<=pdata->prune_set_end)) {

      /* [MC] 20091016 avoid useless work if col+1 == pdata->prune_set_end */
      /* if (!state ||
	  col+1<pdata->prune_set_end ||
	  (col+1==pdata->prune_set_end &&
	   (chs ? fd_member(CMIN(child),pdata->prune_set[col]) :
	   fd_compare_interval(pdata->prune_set[col],CMIN(child),CMAX(child))!=FDI_DISJOINT))) */ 
      SP_BOOL lstate;
      TAGGED cmin = CMIN(child);
      TAGGED cmax = CMAX(child);
	if (dvar_is_interval(dv) ? FALSE :
	    cmin==cmax ? !fd_member(cmin,set) :
	    fd_compare_interval(set,cmin,cmax)==FDI_DISJOINT) {
	  lstate = FALSE;
	} else if (NODE(child) == -1) {
	  lstate = TRUE;
	} else {
	  lstate = eval_dag(w,NODE(child),pdata);
	}
      /* update state of current node */
      if (lstate) {
	int i = pdata->prune_set_end;
	pdata->prune_set[col] = fd_subtract_interval(w,pdata->prune_set[col],cmin,cmax);
	
	/* [MA] 20101014: Isn't this loop unnecessary? Taken care of by the recursion? */
	if (i-1==col) {
	  while (i>0 && (pdata->prune_set[i-1]==EmptySet || dvar_is_integer(DVAR(i-1))))
	    i--;
	  pdata->prune_set_end = i;
	}
	if (state)
	  pdata->entailed = FALSE;
	state = TRUE;
      }
      child++;
    }
  }
  /* record state */
    if (state)
      DATErow(node) = pdata->true_date;
    else {
      DATErow(node) = pdata->false_date;
#if CASE_INCF
      false_add(pdata,node);
#endif /* CASE_INCF */
    }
  return state;
}

#if CASE_STAR
static int eval_dag_star MAGIC (HIDDEN_PROTO Argdecl,
				int node,
				struct case_data *pdata)
{
  unsigned long date = DATErow(node);
  int col = VAR(node);
  int state = FALSE;
  
  SP_ASSERT(0 <= node && node < pdata->nnodes);

  if (SAFE(node)) {
    if (date & 0x1) {		/* TRUE or unknown */
      if (date == pdata->true_date) {
	prune_store_prune_sets(w, pdata, col+1);
	return TRUE;
      }
#if CASE_INC
      if (col>=pdata->prune_set_end && date >= LATEST_DATErow(col)) {
	DATErow(node) = pdata->true_date;
	prune_store_prune_sets(w, pdata, col+1);
	return TRUE;
      }
#endif /* CASE_INC */
    } else {			/* FALSE or unknown */
      if (date == pdata->false_date)
	return FALSE;
#if CASE_INCF
      {
	unsigned long fsp = FALSE_SPARSErow(node);
  
	if (fsp < pdata->false_nodes.cardinality && FALSE_DENSErow(fsp)==node) {
	  DATErow(node) = pdata->false_date;
	  return FALSE;
	}
      }
#endif /* CASE_INCF */
    }
  }
  {
    Dvar dv = DVAR(col);
    int child = CHILD(node);
    int child_end = CHILD_END(node);
    TAGGED set = pdata->cache_set[col];
    TAGGED min = dvar_min_t(dv);
    TAGGED max = dvar_max_t(dv);

    int degree = DEGREE(col);

    if (degree > 0) {
      min = MakeSmall(SMIN(col));
      max = MakeSmall(SMAX(col));
    }

    if (min!=CMIN(child)) {
      /* dichotomic search for first child */
      int sup = child_end;
      while (child<sup) {
	int mid = (child+sup)>>1;
	if (FDgt(min,CMAX(mid)))
	  child = mid+1;
	else
	  sup = mid;
      }
    }
    
    /* scan the compatible children */
    /* [MA] I am not sure that !SAFE(node) below is really safe. Investigate! */
    while (child < child_end &&
	   FDle(CMIN(child),max) &&
	   (!SAFE(node) ||
	    !state || col+1<=pdata->prune_set_end)) {

      /* [MC] 20091016 avoid useless work if col+1 == pdata->prune_set_end */
      /* if (!state ||
	  col+1<pdata->prune_set_end ||
	  (col+1==pdata->prune_set_end &&
	   (chs ? fd_member(CMIN(child),pdata->prune_set[col]) :
	   fd_compare_interval(pdata->prune_set[col],CMIN(child),CMAX(child))!=FDI_DISJOINT))) */ 
      SP_BOOL lstate;
      TAGGED cmin = CMIN(child);
      TAGGED cmax = CMAX(child);

      SP_ASSERT(!pdata->store.nqueue);

      if (degree == 0) {
	if (dvar_is_interval(dv) ? FALSE :
	    cmin==cmax ? !fd_member(cmin,set) :
	    fd_compare_interval(set,cmin,cmax)==FDI_DISJOINT) {
	  lstate = FALSE;
	} else {
	  unsigned long l;
	  lstate = TRUE;
	  
	  for (l = LINEAR(child); lstate && l < LINEAR_END(child); l++) {
	    SP_ASSERT(!LINEAR_STATUS(l));
	    lstate &= initialize_and_enqueue(pdata, l);
	  }

	  if (lstate && pdata->store.nqueue > 0) 
	    lstate &= propagate(pdata, col);

	  if (lstate) {
	    if (NODE(child) == -1) {
	      if (pdata->store.nactive>0)
		pdata->entailed = FALSE;
	      lstate = TRUE;
	      prune_store_prune_sets(w, pdata, pdata->nvars);
	    } else {
	      lstate = eval_dag_star(w,NODE(child),pdata);
	    }
	  }

	  if (!lstate) { /* failure: cleanup */
	    while (pdata->store.nqueue)
	      queue_pop(pdata);
	  }

	  while (pdata->trail.size && LATEST_TRAIL_DATE() == col)
	    untrail(pdata);

	  SP_ASSERT(!pdata->trail.size || LATEST_TRAIL_DATE() < col);

	  for (l = LINEAR(child); l < LINEAR_END(child); l++) {
	    if (LINEAR_STATUS(l)) {
	      DEACTIVATE(l);
	      SP_ASSERT(!LINEAR_STATUS(l));
	    }
	  }
	}
      } else { /* degree > 0 */
	long smin0 = SMIN(col);
	long smax0 = SMAX(col);
	TAGGED t_smin0 = MakeSmall(smin0);
	TAGGED t_smax0 = MakeSmall(smax0);
	
	TAGGED pset = fd_intersection_interval(w, set, t_smin0, t_smax0);
	
	int cmp = fd_compare_interval(pset, cmin, cmax);
	
	SP_ASSERT(DEGREE(col));
	
	if (cmp == FDI_DISJOINT) {
	  lstate = FALSE;
	} else {
	  long smin, smax;
	  unsigned long l;
	  TAGGED cons;
	  
	  switch (cmp) {
	  case FDI_SUBSET:
	  case FDI_EQUAL:
	    smin = GetSmall(FDgt(cmin,t_smin0) ? cmin : t_smin0);
	    smax = GetSmall(FDgt(cmax,t_smax0) ? t_smax0 : cmax);
	    break;
	  default: /* intersection */
	    cons = fd_interval(w, cmin, cmax);
	    smin = GetSmall(fd_intersection_min(set, cons));
	    smax = GetSmall(fd_intersection_max(set, cons));	    
	    smin = FDMAX(smin, smin0);
	    smax = FDMIN(smax, smax0);
	    break;
	  }
	  
	  lstate = TRUE;
	  
	  if (smin > smin0)
	    lstate &= update_and_enqueue(pdata, col, T_LOWER, smin0, smin, 
					 col, pdata->nlinears);
	  if (lstate && smax < smax0)
	    lstate &= update_and_enqueue(pdata, col, T_UPPER, smax0, smax, 
					 col, pdata->nlinears);

	  for (l = LINEAR(child); lstate && l < LINEAR_END(child); l++) {
	    SP_ASSERT(!LINEAR_STATUS(l));
	    lstate &= initialize_and_enqueue(pdata, l);
	  }

	  if (lstate && pdata->store.nqueue > 0) 
	    lstate &= propagate(pdata, col);

	  if (lstate) {
	    if (NODE(child) == -1) { /* leaf node: prune the resulting domains */
	      prune_store_prune_sets(w, pdata, pdata->nvars);
	      if (pdata->store.nactive>0)
		pdata->entailed = FALSE;
	    } else {
	      lstate &= eval_dag_star(w,NODE(child),pdata);
	    }
	  }

	  if (!lstate) { /* failure: cleanup */
	    while (pdata->store.nqueue)
	      queue_pop(pdata);
	  }

	  while (pdata->trail.size && LATEST_TRAIL_DATE() == col)
	    untrail(pdata);

	  SP_ASSERT(!pdata->trail.size || LATEST_TRAIL_DATE() < col);

	  for (l = LINEAR(child); l < LINEAR_END(child); l++) {
	    if (LINEAR_STATUS(l)) {
	      DEACTIVATE(l);
	      SP_ASSERT(!LINEAR_STATUS(l));
	    }
	  }
	}
      }

      SP_ASSERT(!pdata->store.nqueue);

      /* update state of current node */
      if (lstate) {
	int i = pdata->prune_set_end;
	if (degree == 0) {
	  pdata->prune_set[col] = fd_subtract_interval(w,pdata->prune_set[col],cmin,cmax);
	}

	/* [MA] 20101014: Isn't this loop unnecessary? Taken care of by the recursion? */
	if (i-1==col) {
	  while (i>0 
		 && (pdata->prune_set[i-1]==EmptySet 
		     || (dvar_is_integer(DVAR(i-1)) 
			 && DEGREE(i-1) == 0
			 )))
	    i--;
	  pdata->prune_set_end = i;
	}
	if (state)
	  pdata->entailed = FALSE;
	state = TRUE;
      }
      child++;
    }
  }
  /* record state */
  if (SAFE(node)) {
    if (state) {
      DATErow(node) = pdata->true_date;
    } else {
      DATErow(node) = pdata->false_date;
#if CASE_INCF
      false_add(pdata,node);
#endif /* CASE_INCF */
    }
  }
  return state;
}

#endif /* CASE_STAR */

#if CASE_STAR

/* Precondition: safe(node), for all nodes */
static int dfs_safe(struct case_data *pdata, int node, int depth, int lmax) {
  int lmin = depth;
  
  long child;  
  for (child = CHILD(node); child < CHILD_END(node); child++) {
    long linear;
    SP_BOOL non_leaf = NODE(child) > -1;

    for (linear=LINEAR(child); linear < LINEAR_END(child); linear++) {
      int i;
      long *x = LINEAR_X(linear);

      for (i=0; i<LINEAR_LENGTH(linear); i++) {
	lmin = FDMIN(lmin, x[i]);
	
	if (non_leaf) 
	  lmax = FDMAX(lmax, x[i]);
      }
    }

    if (non_leaf) 
      lmin = FDMIN(lmin, dfs_safe(pdata, NODE(child), depth+1, lmax));
  }

  if (lmin < depth || depth <= lmax)
    SAFE(node) = FALSE;

  return lmin;
}

#endif /* CASE_STAR */


/*
   '$fd_case'(+State0, -State, -Actions) :-
   State0 = State = state(f(NVars,NNodes,NChildren,TVars,Dag,On,Prune),EntailmentCtr,_Handle,Stamp)
 */
void SPCDECL
prolog_fd_case MAGIC (HIDDEN_PROTO
		      SP_term_ref State0,
		      SP_term_ref State,
		      SP_term_ref Actions)
{
  WAMENV;
  struct case_data *pdata;
  int i, j, row, nrows, nvars, nnodes, nchildren;
#if CASE_STAR
  unsigned int nlinears = 0;
#endif /* CASE_STAR */
  int ent = -1;
  TAGGED item, tmp, state, handle;
  SP_BOOL committed;
  char *ptr;
  
  w->numstack_end = NULL;
/*    X(0) = RefTerm(State0); */
  (void)State0;
  dvar_export_start(w);
  RefTerm(State) = fd_static_output_state(w,&handle,&committed);

  if (!IsVar(handle)) {		/* got [Flag | '$free'(Ptr)] */
    pdata = Pdata(struct case_data,handle);
    nrows = pdata->nrows;
    nvars = pdata->nvars;
    nnodes = pdata->nnodes;
    nlinears = pdata->nlinears;
  } else {			/* build persistent state */
    int child_index, node;
#if CASE_STAR
    int linear_index;
#endif /* CASE_STAR */
    TAGGED rows, tvars, dag, *h;
    size_t total_size;
    
    DerefArg(state,X(0),1);
    DerefArg(tmp,state,1); 
    nvars = GetSmall(tmp);
    DerefArg(tmp,state,2); 
    nnodes = GetSmall(tmp);
    DerefArg(tmp,state,3); 
    nchildren = GetSmall(tmp);
    DerefArg(tmp,state,4); 
    nrows = fd_list_length(tmp);
#if CASE_STAR
    DerefArg(tmp,state,5);
    nlinears = GetSmall(tmp);
#endif /* CASE_STAR */
    total_size = nvars*sizeof(struct dvar)+             /* dvar */
      nvars*2*sizeof(TAGGED)+	                        /* prune_set */
				                        /* cache_set */
      nvars*2*sizeof(long)+                             /* control */
				                        /* on */
      nrows*2*nvars*sizeof(long)+                       /* latest_date */
				                        /* latest_size */
      nrows*nnodes*sizeof(long)+                        /* dag_node.date */
      nnodes*4*sizeof(long)+	                        /* dag_node.id */
				                        /* dag_node.var_index */
				                        /* dag_node.child_index */
				                        /* dag_node.child_end */
      nchildren*3*sizeof(long)+                         /* child.min */
				                        /* child.max */
				                        /* child.node_index */
#if CASE_STAR
      nnodes*sizeof(SP_BOOL)+                           /* dag_node.safe */
      nchildren*2*sizeof(unsigned long)+                /* child.linear_index */
                                                        /* child.linear_end */
      nlinears*2*nvars*sizeof(long)+                    /* linear.a */
                                                        /* linear.I */
      nlinears*3*nvars*sizeof(long)+                    /* linear.x */
                                                        /* linear.heap */
                                                        /* linear.heapx */
      nlinears*3*sizeof(long)+                          /* linear.b */
                                                        /* linear.F */	     
                                                        /* linear.E */		
      nlinears*sizeof(unsigned long)+                   /* linear.length */
      nlinears*sizeof(linear_status)+                   /* linear.status */	
      nvars*2*sizeof(long)+                             /* store.min */
                                                        /* store.max */	     
      nvars*sizeof(unsigned long)+                      /* store.vars */
      nlinears*sizeof(unsigned long)+                   /* store.queue */
      nvars*sizeof(unsigned long)+                      /* degree */
      nlinears*2*nvars*sizeof(unsigned long)+           /* linears */
                                                        /* indices */
#endif /* CASE_STAR */
#if CASE_INCF
      nrows*2*nnodes*sizeof(unsigned long) +
                             				/* false_nodes.dense */
                            				/* false_nodes.sparse */
#endif /* CASE_INCF */
      nrows*sizeof(long);	                        /* next */

    pdata = Palloc(struct case_data, total_size, handle);
    pdata->destructor = case_destructor;
    pdata->daemon = case_daemon;
    FD_STORE_SPENV(pdata->spenv);
    pdata->stamp = 0;
    pdata->nrefs = 2*nrows*nvars+nrows;
#if CASE_INCF
    pdata->nrefs += nrows;
#endif /* CASE_INCF */
    pdata->refbase = SP_alloc_globrefs(pdata->nrefs);
    pdata->nrows = nrows;
    pdata->nvars = nvars;
    pdata->nnodes = nnodes;
#if CASE_STAR
    pdata->nlinears = nlinears;
    pdata->trail.size = 0;
    pdata->trail.max_size = nvars*nvars*NTRAILED;
#endif /* CASE_STAR */
    pdata->false_date = 0L;
    pdata->true_date = 1L;
    ptr = (char *)(pdata+1);
    pdata->dvar = (Dvar)ptr; ptr += nvars*sizeof(struct dvar);
    pdata->prune_set = (TAGGED *)ptr; ptr += nvars*sizeof(TAGGED);
    pdata->cache_set = (TAGGED *)ptr; ptr += nvars*sizeof(TAGGED);
    pdata->control = (unsigned long *)ptr; ptr += nvars*sizeof(long);
    pdata->on = (unsigned long *)ptr; ptr += nvars*sizeof(long);
    pdata->latest_date = (unsigned long *)ptr; ptr += nrows*nvars*sizeof(long);
    pdata->latest_size = (long *)ptr; ptr += nrows*nvars*sizeof(long);
    pdata->dag_node.date = (unsigned long *)ptr; ptr += nrows*nnodes*sizeof(long);
    pdata->dag_node.id = (long *)ptr; ptr += nnodes*sizeof(long);
    pdata->dag_node.var_index = (long *)ptr; ptr += nnodes*sizeof(long);
    pdata->dag_node.child_index = (long *)ptr; ptr += nnodes*sizeof(long);
    pdata->dag_node.child_end = (long *)ptr; ptr += nnodes*sizeof(long);
    pdata->child.min = (TAGGED *)ptr; ptr += nchildren*sizeof(long);
    pdata->child.max = (TAGGED *)ptr; ptr += nchildren*sizeof(long);
    pdata->child.node_index = (long *)ptr; ptr += nchildren*sizeof(long);
    pdata->next = (long *)ptr; ptr += nrows*sizeof(long);
#if CASE_INCF
    pdata->false_nodes.dense = (unsigned long *)ptr; ptr += nrows*nnodes*sizeof(unsigned long);
    pdata->false_nodes.sparse = (unsigned long *)ptr; ptr += nrows*nnodes*sizeof(unsigned long);
#endif /* CASE_INCF */
#if CASE_STAR
    pdata->child.linear_index = (unsigned long *)ptr; ptr += nchildren*sizeof(unsigned long);
    pdata->child.linear_end = (unsigned long *)ptr; ptr += nchildren*sizeof(unsigned long);
    pdata->linear.a = (long *)ptr; ptr += nlinears*nvars*sizeof(long);
    pdata->linear.I = (long *)ptr; ptr += nlinears*nvars*sizeof(long);
    pdata->linear.x = (long *)ptr; ptr += nlinears*nvars*sizeof(long);
    pdata->linear.heap = (unsigned long *)ptr; ptr += nlinears*nvars*sizeof(unsigned long);
    pdata->linear.heapx = (unsigned long *)ptr; ptr += nlinears*nvars*sizeof(unsigned long);
    pdata->linear.b = (long *)ptr; ptr += nlinears*sizeof(long);
    pdata->linear.E = (long *)ptr; ptr += nlinears*sizeof(long);
    pdata->linear.F = (long *)ptr; ptr += nlinears*sizeof(long);
    pdata->linear.length = (unsigned long *)ptr; ptr += nlinears*sizeof(unsigned long);
    pdata->store.min = (long *)ptr; ptr += nvars*sizeof(long);
    pdata->store.max = (long *)ptr; ptr += nvars*sizeof(long);
    pdata->store.queue = (unsigned long *)ptr; ptr += nlinears*sizeof(unsigned long);
    pdata->store.vars = (unsigned long *)ptr; ptr += nvars*sizeof(unsigned long);
    pdata->degree = (unsigned long *)ptr; ptr += nvars*sizeof(unsigned long);
    pdata->linears = (unsigned long *)ptr; ptr += nlinears*nvars*sizeof(unsigned long);
    pdata->indices = (unsigned long *)ptr; ptr += nlinears*nvars*sizeof(unsigned long);
    /* everything above was long aligned! */
    pdata->linear.status = (linear_status *)ptr; ptr += nlinears*sizeof(linear_status);
    pdata->dag_node.safe = (SP_BOOL *)ptr; ptr += nnodes*sizeof(SP_BOOL);
#endif /* CASE_STAR */
    SP_ASSERT(ptr == (char *)(pdata+1)+total_size);
    pdata->first = nrows-1;
    for (i=nrows-1; i>=0; i--)
      pdata->next[i] = i-1;
    DerefArg(state,X(0),1);	/* refresh */
    DerefArg(rows,state,4);
    DerefArg(dag,state,6); 
    
    for (i=0; i<nrows; i++) {
      DerefCar(tvars,rows);
      DerefCdr(rows,rows);
      for (j=0; j<nvars; j++) {
	SP_globref ref = ATTRIBUTE_LOC(i,j);

	DerefCar(item,tvars);
	DerefCdr(tvars,tvars);
	fd_get_var_and_attr(item,ref);
      }
    }

#if CASE_STAR
    for (i=0; i<nvars; i++)
      DEGREE(i) = 0;
#endif /* CASE_STAR */

    /* build the DAG */
    child_index = 0;
#if CASE_STAR
    linear_index = 0;
#endif /* CASE_STAR */
    for (node=0; node<nnodes; node++) {
      TAGGED children, cmin, cmax;

#if CASE_STAR
      SAFE(node) = TRUE;
#endif /* CASE_STAR */

      DerefCar(item,dag);	  /* dagnode(ID,VAR,VARSET,Children,_) */
      DerefCdr(dag,dag);
      DerefArg(tmp,item,1);	  /* node ID */
      ID(node) = GetSmall(tmp);
      DerefArg(tmp,item,2);	  /* var index */
      VAR(node) = GetSmall(tmp);
      CHILD(node) = child_index;
      DerefArg(children,item,4);         /* children */
      while (TagIsLST(children)) {
	TAGGED child, interval, linears, child_id;
	DerefCar(child,children);       /* (min..max)-Linears-Id */
	DerefCdr(children,children);
	DerefArg(tmp,child,1);          /* (min..max)-Linears */       
	DerefArg(interval,tmp,1);
	DerefArg(linears, tmp, 2);
	DerefArg(cmin,interval,1);
	DerefArg(cmax,interval,2);
	DerefArg(child_id,child,2);
	CMIN(child_index) = cmin;
	CMAX(child_index) = cmax;
#if CASE_STAR
	LINEAR(child_index) = linear_index;
	while (TagIsLST(linears)) {
	  TAGGED as, b, linear, xs;
	  int index = 0;

	  DerefCar(linear, linears);     /* scalar_product(as, xs, #=<, b) */
	  DerefCdr(linears, linears);
	  SP_ASSERT(Arity(TagToHeadfunctor(linear)) == 4);
	  DerefArg(as,linear,1);
	  DerefArg(xs,linear,2);
	  DerefArg(b,linear,4);
	      
	  while (TagIsLST(as)) {
	    TAGGED a, x;
	    long x_l;

	    DerefCar(a,as);
	    DerefCdr(as,as);
	    DerefCar(x,xs);
	    DerefCdr(xs,xs);
	    x_l = GetSmall(x);

	    SP_ASSERT(x_l >= 0);

	    LINEAR_A(linear_index)[index] = GetSmall(a);
	    LINEAR_X(linear_index)[index] = x_l;
	    LINEAR_HEAP(linear_index)[index] = index;
	    LINEAR_HEAPX(linear_index)[index] = index;
	    VAR_LINEAR(x_l, DEGREE(x_l)) = linear_index;
	    VAR_LINEAR_INDEX(x_l, DEGREE(x_l)) = index;
	    DEGREE(x_l)++;
	    index++;
	  }

	  LINEAR_B(linear_index) = GetSmall(b);
	  LINEAR_E(linear_index) = 0;
	  LINEAR_F(linear_index) = 0;
	  LINEAR_LENGTH(linear_index) = index;
	  LINEAR_STATUS(linear_index) = 0;

	  SP_ASSERT(LINEAR_LENGTH(linear_index) > 0);

	  linear_index++;
	}

	LINEAR_END(child_index) = linear_index;
#endif /* CASE_STAR */
	NODE(child_index) = (TagIsSmall(child_id) ? GetSmall(child_id) : -1);
	child_index++;
      }
      CHILD_END(node) = child_index;
      for (row=0; row<nrows; row++) {
	DATE(row,node) = -2U;
      }
    }

#if CASE_STAR
    pdata->store.nvars = 0;

    if (nlinears > 0) {
      unsigned long x, x_i;
           
      x_i = 0;
      for (x=0; x<nvars; x++) {
	if (DEGREE(x) > 0) {
	  pdata->store.vars[x_i++] = x;
	}
      }
      
      pdata->store.nvars = x_i;

      dfs_safe(pdata, 0, 0, -1);
    }
#endif /* CASE_STAR */

    /* build control+on info */
    for (i=0; i<2; i++) {
      unsigned long *map;
      TAGGED prune;
      if (i==0) {
	map = pdata->on;
	DerefArg(prune,state,7); 
      } else {
	map = pdata->control;
	DerefArg(prune,state,8); 
      }
      for (j=0; j<nvars; j++) {
	DerefCar(item,prune);
	DerefCdr(prune,prune);
	item = SetArity(item,1);
	if (item==fd.functor_dom)
	  map[j] = CASE_DOM;
	else if (item==fd.functor_min)
	  map[j] = CASE_MIN;
	else if (item==fd.functor_max)
	  map[j] = CASE_MAX;
	else if (item==fd.functor_minmax)
	  map[j] = CASE_MINMAX;
	else if (item==fd.functor_val)
	  map[j] = CASE_VAL;
	else
	  map[j] = CASE_NONE;
      }
    }
    for (i=0; i<nrows; i++) {
      for (j=0; j<nvars; j++) {
	SP_globref ref = ATTRIBUTE_LOC(i,j);
	Dvar dv = DVAR(j);
	
	dvar_init(dv, ref, ref+1);
	LATEST_DATE(i,j) = -1U;
	LATEST_SIZE(i,j) = dvar_value_count(dv);
	switch (pdata->on[j]) {
	case CASE_DOM:
	  dvar_attach_daemon(w, dv, pdata, X(1), fd.functor_dom);
	  break;
	case CASE_MIN:
	  dvar_attach_daemon(w, dv, pdata, X(1), fd.functor_min);
	  break;
	case CASE_MAX:
	  dvar_attach_daemon(w, dv, pdata, X(1), fd.functor_max);
	  break;
	case CASE_MINMAX:
	  dvar_attach_daemon(w, dv, pdata, X(1), fd.functor_minmax);
	  break;
	case CASE_VAL:
	  dvar_attach_daemon(w, dv, pdata, X(1), fd.functor_val);
	  break;
	}
      }
    }
#if CASE_INCF
    for (i=0; i<nrows; i++)
      for (j=0; j<nnodes; j++)
	FALSE_SPARSE(i,j) = -1U;
    RequireHeap(3*nrows,EVAL_ARITY);
    h = w->global_top;
    for (j=0; j<nrows; j++, h+=3) {
      h[0] = functor_Dmutable;
      h[1] = TaggedZero;
      h[2] = TaggedZero;
      FALSE_CARD_MUT(j) = MakeStructure(h);
    }
    w->global_top = h;
#endif /* CASE_INCF */
    RequireHeap(nrows,EVAL_ARITY);
    h = w->global_top;
    for (i=nrows-1; i>=0; i--)
      ENT_FLAG(i) = h[i] = TagREF(h+i);
    w->global_top = h+nrows; 
    CTagToArg(X(0),1) = atom_nil; /* [MC] 3.12: free for GC */
    DerefArg(tmp,X(0),2);	/* ensure entailment ctr is dereffed */
    CTagToArg(X(0),2) = tmp;
  }
  
  /* RESUME */
  pdata->true_date += 2;
  row = pdata->first;

#if CASE_STAR
  if (nlinears > 0) {
    int trail_max_size = pdata->trail.max_size;
    pdata->trail.type = Malloc(trail_max_size, trailed);
    pdata->trail.date = Malloc(trail_max_size, unsigned long);
    pdata->trail.i = Malloc(trail_max_size, unsigned long);
    pdata->trail.j = Malloc(trail_max_size, unsigned long);
    pdata->trail.value = Malloc(trail_max_size, long);
    pdata->trail.size = 0;
  }
#endif /* CASE_STAR */

  while (row != -1) {
#if CASE_STAR
    unsigned int x;
#endif /* CASE_STAR */
    /* This also initializes the pdata->dvar for row. */
    int nnonground = compute_prune_sets(pdata,w,row);

#if CASE_INCF
    pdata->false_nodes.cardinality = GetSmall(RefMutable(FALSE_CARD_MUT(row)));
    pdata->false_nodes.denserow = &FALSE_DENSE(row,0);
    pdata->false_nodes.sparserow = &FALSE_SPARSE(row,0);
#endif /* CASE_INCF */
    pdata->dag_node.daterow = &DATE(row,0);
    pdata->latest_daterow = &LATEST_DATE(row,0);

#if CASE_STAR
    for (x=0; x<pdata->store.nvars; x++) {
      unsigned long x_i = pdata->store.vars[x];
      Dvar dv = DVAR(x_i);
      SP_ASSERT(DEGREE(x_i));
      SMIN(x_i) = dvar_min_l(dv);
      SMAX(x_i) = dvar_max_l(dv);
    }
    pdata->store.nqueue = 0;
    pdata->store.nactive = 0;
#endif /* CASE_STAR */

    /* evaluate the DAG */
    pdata->entailed = TRUE;
#if CASE_STAR
    if (nlinears > 0) {
      if (!eval_dag_star(w,0,pdata))
	goto ret;
    }
    else {
#endif /* CASE_STAR */
      if (!eval_dag(w,0,pdata))
	goto ret;
#if CASE_STAR
    }
#endif /* CASE_STAR */

#if CASE_INCF
    if (RefMutable(FALSE_CARD_MUT(row)) != MakeSmall(pdata->false_nodes.cardinality)) {
      fd_update_mutable(w,MakeSmall(pdata->false_nodes.cardinality),FALSE_CARD_MUT(row));
    }
#endif /* CASE_INCF */
      /* compute pruning acc. to generalization */
    for (i=0; i<pdata->prune_set_end; i++) {
      if (pdata->prune_set[i] != EmptySet) {
	Dvar dv = DVAR(i);

	switch (pdata->control[i]) {
	case CASE_DOM:
	  dvar_prune_set(dv, pdata->prune_set[i],w);
	  break;
	case CASE_MIN:
	  {
	    TAGGED diff = fd_subtract(w,pdata->cache_set[i],pdata->prune_set[i]);
	    dvar_fix_min_t(dv,fd_min(diff));
	    if (pdata->entailed && dvar_compare_set(dv,diff,w)!=FDI_EQUAL)
	      pdata->entailed = FALSE;
	  }
	  break;
	case CASE_MAX:
	  {
	    TAGGED diff = fd_subtract(w,pdata->cache_set[i],pdata->prune_set[i]);
	    dvar_fix_max_t(dv,fd_max(diff));
	    if (pdata->entailed && dvar_compare_set(dv,diff,w)!=FDI_EQUAL)
	      pdata->entailed = FALSE;
	  }
	  break;
	case CASE_MINMAX:
	  {
	    TAGGED diff = fd_subtract(w,pdata->cache_set[i],pdata->prune_set[i]);
	    dvar_fix_interval_t(dv,fd_min(diff),fd_max(diff));
	    if (pdata->entailed && dvar_compare_set(dv,diff,w)!=FDI_EQUAL)
	      pdata->entailed = FALSE;
	  }
	  break;
	case CASE_VAL:
	  {
	    TAGGED diff = fd_subtract(w,pdata->cache_set[i],pdata->prune_set[i]);
	    if (fd_singleton(diff))
	      dvar_fix_value_t(dv,diff);
	    if (pdata->entailed && dvar_compare_set(dv,diff,w)!=FDI_EQUAL)
	      pdata->entailed = FALSE;
	  }
	  break;
	}

	dvar_pruning_done(w,dv);
	if (dvar_is_integer(dv))
	  nnonground--;
      }
    }
    if (pdata->entailed || nnonground==0) { /* do this before any dvar_export()! */
      TAGGED t = ENT_FLAG(row);
      BindHVA(t,atom_nil);
      CTagToArg(X(0),2) -= IStep(1); /* decrement entailent counter */
    }
    /* propagate, update counts -- must do it also for vars that were not pruned */
    for (i=0; i < nvars; i++) {
      Dvar dv = DVAR(i);
      LATEST_DATE(row,i) = pdata->true_date;
      LATEST_SIZE(row,i) = dvar_value_count(dv);
    }
    for (i=0; i < nvars; i++) {
      Dvar dv = DVAR(i);
      dvar_export(w,dv);
    }
    pdata->first = pdata->next[row];
    pdata->next[row] = -2;
    row = pdata->first;
  }
  pdata->first = -1;
  ent = Teqz(CTagToArg(X(0),2));
 ret:

#if CASE_STAR
  if (nlinears > 0) {
    Free(pdata->trail.type); 
    Free(pdata->trail.date); 
    Free(pdata->trail.i); 
    Free(pdata->trail.j); 
    Free(pdata->trail.value); 
  }
#endif /* CASE_STAR */

  if (ent==1)
    Pfree;
  dvar_export_done(w,Actions, ent);
}

